perm filename REVERS.PPR[W82,JMC] blob sn#864730 filedate 1982-01-21 generic text, type T, neo UTF8
the proof REVERS:

(DECL (REV1) |GROUND⊗GROUND→GROUND| CONSTANT)

(AXIOM |∀U V.REV1(U,V)=IF NULL U THEN V ELSE REV1(CDR U,CAR U~V)|)
2. ∀U V.REV1(U,V)=IF NULL U THEN V ELSE REV1(CDR U,CAR U~V)
   deps: NIL

(COMMENTL LNAME DEFINFO)

(∀E PHI |λU.∀V.REV1(U,V)=REVERSE U*V| LISTINDUCTION
 |NIL*([1#1#1]($DEFINFO*NIL*$DEFINFO*NIL*$DEFINFO**SIMPINFO*NIL))*NIL*
  ([1#1#2](&DEFINFO*NIL**SIMPINFO*NIL))*NIL| SORTINFO)
4. (∀X U.(∀V.REV1(U,V)=REVERSE U*V)⊃(∀V.REV1(U,X~V)=REVERSE U*X~V))⊃
    (∀U V.REV1(U,V)=REVERSE U*V)
   deps: NIL

(ASSUME |∀V.REV1(U,V)=REVERSE U*V|)
5. ∀V.REV1(U,V)=REVERSE U*V
   deps: (5)

(TRW |REV1(U,X~V)| |5| SORTINFO)
6. REV1(U,X~V)=REVERSE U*X~V
   deps: (5)

(∀I (V) 6)
7. ∀V.REV1(U,X~V)=REVERSE U*X~V
   deps: (5)

(CI (5) 7 |NIL|)
8. (∀V.REV1(U,V)=REVERSE U*V)⊃(∀V.REV1(U,X~V)=REVERSE U*X~V)
   deps: NIL

(∀I (X U) 8)
9. ∀X U.(∀V.REV1(U,V)=REVERSE U*V)⊃(∀V.REV1(U,X~V)=REVERSE U*X~V)
   deps: NIL

(RW 4 |$9*NIL|)
10. ∀U V.REV1(U,V)=REVERSE U*V
    deps: NIL